
@article{Manolios2006,
author = {Manolios, P. and Zhang, Y.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Manolios, Zhang/Manolios, Zhang - 2006 - Implementing survey propagation on graphics processing units.pdf:pdf},
journal = {Lecture Notes in Computer Science},
pages = {311},
publisher = {Springer},
title = {{Implementing survey propagation on graphics processing units}},
volume = {4121},
year = {2006}
}
@misc{Mendeley2009,
address = {London},
annote = {Double click on the entry on the left to view the PDF.},
author = {Mendeley},
booktitle = {Mendeley Desktop},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Mendeley/Mendeley - 2009 - Getting Started with Mendeley.pdf:pdf},
keywords = {Mendeley},
publisher = {Mendeley Ltd.},
title = {{Getting Started with Mendeley}},
url = {http://www.mendeley.com},
year = {2009}
}
@inproceedings{Hamadi,
author = {Hamadi, Youssef},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Hamadi/Hamadi - Unknown - From SAT to Parallel SAT Solving.pdf:pdf},
keywords = {SAT},
mendeley-tags = {SAT},
title = {{From SAT to Parallel SAT Solving}}
}
@misc{Mendeley2009a,
address = {London},
annote = {Double click on the entry on the left to view the PDF.},
author = {Mendeley},
booktitle = {Mendeley Desktop},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Mendeley/Mendeley - 2009 - Getting Started with Mendeley.pdf:pdf},
keywords = {Mendeley},
publisher = {Mendeley Ltd.},
title = {{Getting Started with Mendeley}},
year = {2009}
}
@article{Chrabakh2003,
author = {Chrabakh, W. and Wolski, R.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Chrabakh, Wolski/Chrabakh, Wolski - 2003 - Gradsat A parallel sat solver for the grid.pdf:pdf},
journal = {Proceedings of IEEE SC03},
keywords = {SAT,computational grid,distributed,parallel,satis abilty},
mendeley-tags = {SAT},
publisher = {Citeseer},
title = {{Gradsat: A parallel sat solver for the grid}},
year = {2003}
}
@article{Biere2008,
author = {Biere, A.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Biere/Biere - 2008 - PicoSAT essentials.pdf:pdf},
journal = {Journal on Satisfiability, Boolean Modeling and Computation},
keywords = {occurrence lists,proof traces,published may 2008,restarts,revised december 2007,sat solver,submitted october 2007,watched literals},
number = {75-97},
pages = {45},
title = {{PicoSAT essentials}},
volume = {4},
year = {2008}
}
@inproceedings{Clarke1998,
author = {Clarke, E.M. and Jha, S. and Marrero, W.},
booktitle = {Proc. IFIP Working Conference on Programming Concepts and Methods (PROCOMET)},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Clarke, Jha, Marrero/Clarke, Jha, Marrero - 1998 - Using state space exploration and a natural deduction style message derivation engine to verify security protocols.pdf:pdf},
keywords = {Model Checking},
mendeley-tags = {Model Checking},
pages = {87–106},
publisher = {Citeseer},
title = {{Using state space exploration and a natural deduction style message derivation engine to verify security protocols}},
year = {1998}
}
@misc{Biere1999,
author = {Biere, A. and Cimatti, A. and Clark, E. and Zhu, Y.},
booktitle = {Springer},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Biere et al./Biere et al. - 1999 - Symbolic model checking without BDDs.pdf:pdf},
keywords = {Model Checking},
mendeley-tags = {Model Checking},
publisher = {Springer},
title = {{Symbolic model checking without BDDs}},
year = {1999}
}
@misc{Biere1999a,
author = {Biere, A. and Cimatti, A. and Clarke, E.M. and Fujita, M. and Zhu, Y.},
booktitle = {Design Automation Conference},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Biere et al./Biere et al. - 1999 - Symbolic model checking using SAT procedures instead of BDDs.pdf:pdf},
keywords = {Model Checking},
mendeley-tags = {Model Checking},
pages = {317–320},
publisher = {IEEE COMPUTER SOCIETY},
title = {{Symbolic model checking using SAT procedures instead of BDDs}},
year = {1999}
}
@article{Davis1962,
author = {Davis, M and Logemann, G and Loveland, D},
journal = {Communications of the ACM},
number = {7},
pages = {394--397},
title = {{Machine program for theorem proving.}},
volume = {5},
year = {1962}
}
@article{Maneva2007,
author = {Maneva, E. and Mossel, E. and Wainwright, M.J.},
doi = {10.1145/1255443.1255445},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Maneva, Mossel, Wainwright/Maneva, Mossel, Wainwright - 2007 - A new look at survey propagation and its generalizations.pdf:pdf},
issn = {00045411},
journal = {Journal of the ACM (JACM)},
number = {4},
pages = {17},
publisher = {ACM},
title = {{A new look at survey propagation and its generalizations}},
volume = {54},
year = {2007}
}
@article{Braunstein2002,
arxivId = {cs/0212002v4},
author = {Braunstein, A. and Mezard, M. and Zecchina, R.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Braunstein, Mezard, Zecchina/Braunstein, Mezard, Zecchina - 2002 - Survey propagation An algorithm for satisfiability.pdf:pdf},
journal = {Arxiv preprint cs/0212002},
keywords = {Computational Complexity,Statistical Mechanics},
title = {{Survey propagation: An algorithm for satisfiability}},
year = {2002}
}
@article{Gelder2001,
author = {Gelder, Allen Van and Cruz, Santa},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Gelder, Cruz/Gelder, Cruz - 2001 - Extracting (Easily) Checkable Proofs from a Satis ability Solver that Employs both Preorder and Postorder Resolution.pdf:pdf},
journal = {Construction},
pages = {1--10},
title = {{Extracting (Easily) Checkable Proofs from a Satis ability Solver that Employs both Preorder and Postorder Resolution}},
year = {2001}
}
@article{Kroc2002,
author = {Kroc, L. and Sabharwal, A. and Selman, B.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Kroc, Sabharwal, Selman/Kroc, Sabharwal, Selman - 2002 - Survey propagation revisited.pdf:pdf},
journal = {23rd UAI},
pages = {217–226},
publisher = {Citeseer},
title = {{Survey propagation revisited}},
year = {2002}
}
@article{Murphy1999,
author = {Murphy, K. and Weiss, Y. and Jordan, M.I.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Murphy, Weiss, Jordan/Murphy, Weiss, Jordan - 1999 - Loopy belief propagation for approximate inference An empirical study.pdf:pdf},
journal = {Proceedings of Uncertainty in AI},
pages = {467–475},
publisher = {Citeseer},
title = {{Loopy belief propagation for approximate inference: An empirical study}},
year = {1999}
}
@article{Yedidia2001,
author = {Yedidia, J.S. and Freeman, W.T. and Weiss, Y.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Yedidia, Freeman, Weiss/Yedidia, Freeman, Weiss - 2001 - Generalized belief propagation.pdf:pdf},
journal = {In NIPS 13},
title = {{Generalized belief propagation}},
year = {2001}
}
@article{Baldamus2001,
author = {Baldamus, M. and Schroder-Babo, J.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Baldamus, Schroder-Babo/Baldamus, Schroder-Babo - 2001 - p2b A translation utility for linking PROMELA and symbolic model checking (tool paper).pdf:pdf},
journal = {Lecture notes in computer science},
pages = {183–191},
publisher = {Springer},
title = {{p2b: A translation utility for linking PROMELA and symbolic model checking (tool paper)}},
year = {2001}
}
@article{Brat,
author = {Brat, Guillaume and Havelund, Klaus and Park, Seungjoon and Visser, Willem},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Brat et al./Brat et al. - Unknown - Java PathFinder 2.pdf:pdf},
journal = {Analysis},
title = {{Java PathFinder 2}}
}
@article{Clarke2004,
author = {Clarke, Edmund and Kroening, Daniel and Sharygina, Natasha and Yorav, Karen},
doi = {10.1023/B:FORM.0000040025.89719.f3},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Clarke et al./Clarke et al. - 2004 - Predicate Abstraction of ANSI-C Programs Using SAT.pdf:pdf},
issn = {0925-9856},
journal = {Formal Methods in System Design},
keywords = {ansi-c,predicate abstraction,sat},
month = {Сентябрь},
number = {2/3},
pages = {105--127},
title = {{Predicate Abstraction of ANSI-C Programs Using SAT}},
volume = {25},
year = {2004}
}
@inproceedings{Clarke2005,
author = {Clarke, E. and Kroening, D. and Sharygina, N. and Yorav, K.},
booktitle = {TACAS},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Clarke et al./Clarke et al. - 2005 - SATABS SAT-based predicate abstraction for ANSI-C.pdf:pdf},
pages = {570–574},
publisher = {Springer},
title = {{SATABS: SAT-based predicate abstraction for ANSI-C}},
volume = {5},
year = {2005}
}
@article{Een2004,
author = {E\'{e}n, N. and Sorensson, N.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/E\'{e}n, Sorensson/E\'{e}n, Sorensson - 2004 - An extensible SAT-solver.pdf:pdf},
journal = {Lecture notes in computer science},
pages = {502–518},
publisher = {Springer},
title = {{An extensible SAT-solver}},
volume = {2919},
year = {2004}
}
@article{Een2005,
author = {E\'{e}n, N. and Biere, A.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/E\'{e}n, Biere/E\'{e}n, Biere - 2005 - Effective preprocessing in SAT through variable and clause elimination.pdf:pdf},
journal = {Lecture Notes in Computer Science},
pages = {61–75},
publisher = {Springer},
title = {{Effective preprocessing in SAT through variable and clause elimination}},
volume = {3569},
year = {2005}
}
@article{Marques-Silva1999,
author = {Marques-Silva, JP and Sakallah, KA},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Marques-Silva, Sakallah/Marques-Silva, Sakallah - 1999 - GRASP A search algorithm for propositional satisfiability.pdf:pdf},
journal = {IEEE Transactions on Computers},
number = {5},
pages = {506–521},
title = {{GRASP: A search algorithm for propositional satisfiability}},
volume = {48},
year = {1999}
}
@article{Moskewicz,
author = {Moskewicz, Matthew W and Berkeley, U C},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Moskewicz, Berkeley/Moskewicz, Berkeley - Unknown - Chaff Engineering an Efficient SAT Solver.pdf:pdf},
journal = {Electrical Engineering},
keywords = {boolean satisfiability,design verification},
title = {{Chaff : Engineering an Efficient SAT Solver}}
}
@article{Heule2007,
author = {Heule, Marijn and {Van Maaren}, H.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Heule, Van Maaren/Heule, Van Maaren - 2007 - Effective incorporation of double look-ahead procedures.pdf:pdf},
journal = {Lecture Notes in Computer Science},
pages = {258–271},
publisher = {Springer},
title = {{Effective incorporation of double look-ahead procedures}},
volume = {4501},
year = {2007}
}
@article{Kasif1990,
author = {Kasif, Simon},
doi = {10.1016/0004-3702(90)90009-O},
issn = {00043702},
journal = {Artificial Intelligence},
month = {Октябрь},
number = {3},
pages = {275--286},
title = {{On the parallel complexity of discrete relaxation in constraint satisfaction networks}},
volume = {45},
year = {1990}
}

@book{2002,
author = {Хопкрофт, Д. and Мотвани, Р. and Ульман, Д.},
isbn = {5-8459-0261-4},
publisher = {Вильямс М},
title = {{Введение в теорию автоматов, языков и вычислений}},
year = {2002}
}

@book{Sowa2000,
abstract = {Sowa integrates logic, philosophy, linguistics, and computer science into this study of knowledge and its various models and implementations. His definitive new book shows how techniques of artificial intelligence, database design, and object-oriented programming help make knowledge explicit in a form that computer systems can use.},
author = {Sowa, John F},
booktitle = {Knowledge representation logical philosophical and computational foundations},
isbn = {0534949657},
pages = {512},
publisher = {Brooks Cole Publishing Co.},
title = {{Knowledge Representation: Logical, Philosophical, and Computational Foundations}},
year = {2000}
}
@article{Boyd1996,
abstract = {For the success of clinical and translational science, a seamless interoperation is required between clinical and research information technology. Addressing this need, the Michigan Clinical Research Collaboratory (MCRC) was created. The MCRC employed a standards-driven Web Services architecture to create the U-M Honest Broker, which enabled sharing of clinical and research data among medical disciplines and separate institutions. Design objectives were to facilitate sharing of data, maintain a master patient index (MPI), deidentification of data, and routing data to preauthorized destination systems for use in clinical care, research, or both. This article describes the architecture and design of the U-M HB system and the successful demonstration project. Seventy percent of eligible patients were recruited for a prospective study examining the correlation between interventional cardiac catheterizations and depression. The U-M Honest Broker delivered on the promise of using structured clinical knowledge shared among providers to help clinical and translational research.},
author = {Boyd, Andrew D and Saxman, Paul R and Hunscher, Dale A and Smith, Kevin A and Morris, Timothy D and Kaston, Michelle and Bayoff, Frederick and Rogers, Bruce and Hayes, Pamela and Rajeev, Namrata and Kline-Rogers, Eva and Eagle, Kim and Clauw, Daniel and Greden, John F and Green, Lee A and Athey, Brian D},
doi = {10.1197/jamia.M2985},
issn = {1527-974X},
journal = {Journal of the American Medical Informatics Association : JAMIA},
keywords = {Biomedical Research,Biomedical Research: organization \& administration,Biomedical Research: statistics \& numerical data,Computer Security,Humans,Information Dissemination,Information Systems,Interdisciplinary Communication,Interinstitutional Relations,Internet,Michigan,User-Computer Interface},
number = {6},
pages = {784--91},
pmid = {19717803},
title = {{GRASP}},
volume = {16},
year = {1996}
}
@article{1976,
author = {Цейтин, Г.С.},
doi = {10.1007/BF01903823},
issn = {0133-3852},
journal = {Записки научных семинаров ПОМИ},
month = {Декабрь},
number = {4},
pages = {234–259},
publisher = {Санкт-Петербургское отделение Математического института им. ВА Стеклова РАН},
title = {{О сложности вывода в исчислении высказываний}},
volume = {8},
year = {1968}
}
@inproceedings{Plaza2006,
author = {Plaza, Stephen and Kountanis, Ian and Andraus, Zaher and Bertacco, Valeria and Mudge, Trevor},
booktitle = {International Workshop on Logic Synthesis},
publisher = {Citeseer},
title = {{Advances and Insights into Parallel SAT Solving}},
year = {2006}
}
@article{Bohm1996,
author = {B\"{o}hm, Max and Speckenmeyer, Ewald},
doi = {10.1007/BF02127976},
issn = {1012-2443},
journal = {Annals of Mathematics and Artificial Intelligence},
month = {Сентябрь},
number = {2},
pages = {381--400},
title = {{A fast parallel SAT-solver — efficient workload balancing}},
volume = {17},
year = {1996}
}
@article{Een,
author = {Een, Niklas},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Een/Een - Unknown - Minisat v1. 13-a sat solver with conflict-clause minimization.pdf:pdf},
journal = {SAT},
pages = {2--3},
title = {{Minisat v1. 13-a sat solver with conflict-clause minimization}}
}
@book{Cook1971,
address = {New York, New York, USA},
author = {Cook, Stephen A.},
booktitle = {Proceedings of the third annual ACM symposium on Theory of computing - STOC '71},
doi = {10.1145/800157.805047},
pages = {151--158},
publisher = {ACM Press},
title = {{The complexity of theorem-proving procedures}},
year = {1971}
}
@article{Deleau,
author = {Deleau, H. and Jaillet, Christophe and Krajecki, M.},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Deleau, Jaillet, Krajecki/Deleau, Jaillet, Krajecki - Unknown - GPU4SAT solving the SAT problem on GPU.pdf:pdf},
journal = {para08.idi.ntnu.no},
keywords = {gpu,parallel programming,sat problem,simd model},
title = {{GPU4SAT: solving the SAT problem on GPU}},
}
@misc{Zhongwen2005,
author = {Zhongwen, LUO and Zhengping, Yang and Hongzhi, LIU and Weixian, LV},
booktitle = {Environment},
file = {:C$\backslash$:/Documents and Settings/Евнений/Мои документы/Mendeley Desktop/Zhongwen et al./Zhongwen et al. - 2005 - GA Computation of 3-SAT problem on Graphic Process Unit.pdf:pdf},
keywords = {3-sat,genetic algorithm,graphic process unit},
pages = {7--11},
publisher = {ISICA},
title = {{GA Computation of 3-SAT problem on Graphic Process Unit}},
volume = {1},
year = {2005}
}
